\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type.
\\[0ex]es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Leftrightarrow$
\\[0ex]\{\=($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)\+
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ $i$ $\vee$ isrcv($e$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ ${\it da}$(kind($e$))?Top)\}
\-
\end{tabbing}